T:Type, P:(T), L1, L2:T List.
no_repeats(T;L1)
 (x:T. (x  L2)  (x  L1) & P(x)) & (x, y:T. x before y  L2  x before y  L1)
 filter(P;L1) = L2 

latex

Definitions	x:AB(x), (x  l), b, P & Q, P  Q, x:AB(x), x:A. B(x), x before y  l, P  Q, , a<b, s = t, A, no_repeats(T;l), t  T, P  Q, Type, , type List, Prop, f(a), Void, False
Lemmas	no repeats iff, iff wf, l member wf, assert wf, l before wf, no repeats wf, bool wf, filter-equals